/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BASB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRKB30
␈↓ α∧␈↓␈↓ u1


␈↓ α∧␈↓α␈↓ αIAN INDUCTION PRINCIPLE FOR CYCLIC LIST STRUCTURES AND GRAPHS

␈↓ α∧␈↓α␈↓ ¬
John McCarthy, Stanford University

␈↓ α∧␈↓␈↓ αTCyclic␈α∂or␈α∂re-entrant␈α∂list␈α∂structures␈α∂are␈α∂second␈α∞class␈α∂citizens␈α∂in␈α∂most␈α∂LISPs.␈α∂ They␈α∂can␈α∞be

␈↓ α∧␈↓created␈α⊂using␈α⊂␈↓↓rplaca␈↓␈α⊃and␈α⊂␈↓↓rplacd,␈↓␈α⊂but␈α⊃most␈α⊂LISPs␈α⊂can't␈α⊂print␈α⊃them,␈α⊂the␈α⊂standard␈α⊃theories␈α⊂for

␈↓ α∧␈↓proving␈αassertions␈αabout␈αprograms␈αdon't␈αapply␈α
to␈αthem,␈αand␈αspecial␈αprograms␈αhave␈αto␈α
be␈αwritten

␈↓ α∧␈↓to␈α
compute␈α
with␈α
them.␈α
 The␈αmain␈α
characteristic␈α
of␈α
such␈α
programs␈αis␈α
that␈α
in␈α
order␈α
to␈αavoid␈α
infinite

␈↓ α∧␈↓recursions,␈αthey␈αmust␈αcarry␈αalong␈αa␈αlist␈αof␈αnodes␈αalready␈αvisited␈αthat␈αis␈αcompared␈αwith␈αthe␈αcurrent

␈↓ α∧␈↓node.  This provides the essential clue to finding a new induction principle that applies to them.

␈↓ α∧␈↓␈↓ αTFrom␈α
another␈α
point␈α
of␈α
view␈α
we␈α
are␈α
talking␈α
about␈α
finite␈α
binary␈α
directed␈α
graphs,␈α∞which␈α
we

␈↓ α∧␈↓shall␈α
call␈α
fbd␈α
graphs␈α
for␈α
short.␈α
 Looked␈α
at␈α
set-theoretically,␈α
an␈α
fbd␈α
graph␈α
is␈α
a␈α
finite␈α
set␈α
␈↓↓A,␈↓␈α
a␈α
unary

␈↓ α∧␈↓predicate ␈↓↓atom,␈↓ and two maps ␈↓↓car␈↓ and ␈↓↓cdr␈↓ from the non-atoms into ␈↓↓A.␈↓

␈↓ α∧␈↓␈↓ αTA␈α
full␈α
theory␈α
of␈α
programs␈α
on␈αfbd␈α
graphs␈α
would␈α
include␈α
operations␈α
that␈α
produce␈αand␈α
change

␈↓ α∧␈↓graphs.␈α We␈αdon't␈αhave␈αthat␈αyet,␈αand␈α
the␈αformalism␈αof␈α(Morris␈αand␈αSchwarz␈α1980)␈αwhich␈α
includes

␈↓ α∧␈↓such␈αoperations␈α
may␈αnot␈α
be␈αeasy␈α
to␈αaxiomatize.␈α However,␈α
we␈αdo␈α
have␈αan␈α
axiom␈αschema␈α
in␈αfirst

␈↓ α∧␈↓order␈αlogic␈α
that␈αpermits␈αcomputer␈α
checkable␈αfirst␈αorder␈α
logic␈αproofs␈αof␈α
facts␈αabout␈α
programs␈αthat

␈↓ α∧␈↓traverse␈α
fbd␈α
graphs␈α
using␈αoperations␈α
␈↓↓car,␈↓␈α
␈↓↓cdr,␈↓␈α
equality␈αand␈α
the␈α
test␈α
for␈α␈↓↓atom␈↓␈α
on␈α
the␈α
graph␈αand

␈↓ α∧␈↓ordinary LISP operations on lists of nodes and other entities.

␈↓ α∧␈↓␈↓ αTWe␈α⊃will␈α⊃use␈α⊃␈↓↓x␈↓␈α⊂for␈α⊃a␈α⊃variable␈α⊃ranging␈α⊃over␈α⊂nodes␈α⊃in␈α⊃fbd␈α⊃graphs␈α⊂and␈α⊃␈↓↓u,␈↓␈α⊃␈↓↓v␈↓␈α⊃and␈α⊃␈↓↓w␈↓␈α⊂for

␈↓ α∧␈↓variables␈αranging␈α
over␈αlists␈α
whose␈αelements␈α
may␈αbe␈α
such␈αnodes␈α
but␈αwhich␈α
terminate␈αin␈α
NIL␈αjust

␈↓ α∧␈↓like␈αthe␈αusual␈αLISP␈αlists.␈α We␈αalso␈αuse␈αthe␈αnotation␈αof␈α(McCarthy␈αand␈αTalcott␈α1980)␈αof␈α␈↓αa␈↓␈αfor␈α␈↓↓car,␈↓

␈↓ α∧␈↓␈↓αd␈↓ for ␈↓↓cdr,␈↓ infixed . for ␈↓↓cons␈↓ and ␈↓αa␈↓t for ␈↓↓atom.␈↓

␈↓ α∧␈↓␈↓ αTUnlike␈α∞trees,␈α∂fbd␈α∞graphs␈α∞are␈α∂not␈α∞inductively␈α∞defined␈α∂structures.␈α∞ Nevertheless,␈α∞there␈α∂is␈α∞an

␈↓ α∧␈↓axiom schema that we will call the graph induction schema, namely

␈↓ α∧␈↓1)␈↓ αt ␈↓↓∀x u.(␈↓αa␈↓↓t x ∨ x ε u ∨ ␈↓	F␈↓↓(␈↓αa␈↓↓ x, x.u) ∧ ␈↓	F␈↓↓(␈↓αd␈↓↓ x, x.u) ⊃ ␈↓	F␈↓↓(x,u)) ⊃ ∀x u.␈↓	F␈↓↓(x,u)␈↓.
␈↓ α∧␈↓␈↓ u2


␈↓ α∧␈↓The␈α∞variable␈α∂␈↓↓u␈↓␈α∞in␈α∞the␈α∂schema␈α∞is␈α∞a␈α∂list␈α∞of␈α∂nodes␈α∞for␈α∞which␈α∂nothing␈α∞has␈α∞to␈α∂be␈α∞proved,␈α∂and␈α∞the

␈↓ α∧␈↓finiteness␈αof␈αthe␈αgraph␈αinsures␈αthat␈αas␈αwe␈αgo␈αdown␈αin␈αthe␈αgraph␈αwe␈αeventually␈αhit␈αeither␈αatoms␈α
or

␈↓ α∧␈↓nodes␈α
already␈α
examined.␈α
 It␈αmay␈α
help␈α
understanding␈α
to␈α
note␈αthat␈α
the␈α
schema␈α
corresponds␈α
to␈αthe

␈↓ α∧␈↓termination of the LISP-type predicate ␈↓↓isfbdg␈↓ (for "is finite binary directed graph") defined by

␈↓ α∧␈↓␈↓ αT␈↓↓isfbdg x ← isfbdg1[x,␈↓NIL␈↓↓]␈↓,

␈↓ α∧␈↓␈↓ αT␈↓↓isfbdg1[x,u] ← ␈↓αa␈↓↓t x ∨ x ε u ∨ isfbdg1[␈↓αa␈↓↓ x, x.u] ∧ isfbdg1[␈↓αd␈↓↓ x, x.u]␈↓.

␈↓ α∧␈↓The␈α⊃statement␈α⊃that␈α⊃␈↓↓isfbdg␈↓␈α⊃always␈α⊃terminates␈α⊂corresponds␈α⊃to␈α⊃the␈α⊃local␈α⊃finiteness␈α⊃of␈α⊃the␈α⊂graph.

␈↓ α∧␈↓Starting from any vertex, only a finite number can be reached.

␈↓ α∧␈↓␈↓ αTThis␈αcan␈αbe␈αcompared␈αwith␈αthe␈αinduction␈αschema␈αfor␈αS-expressions,␈αi.e.␈αfinite␈α
binary␈αtrees,

␈↓ α∧␈↓namely

␈↓ α∧␈↓2)␈↓ αt ␈↓↓∀x.(␈↓αa␈↓↓t x ∨ ␈↓	F␈↓↓(␈↓αa␈↓↓ x) ∧ ␈↓	F␈↓↓(␈↓αd␈↓↓ x) ⊃ ␈↓	F␈↓↓(x)) ⊃ ∀x.␈↓	F␈↓↓(x)␈↓.

␈↓ α∧␈↓The␈αPeano␈αaxiom␈α
schema␈αfor␈αnatural␈α
numbers␈αmay␈αbe␈αwritten␈α
in␈αa␈αcorresponding␈α
"down␈αgoing"

␈↓ α∧␈↓form, namely

␈↓ α∧␈↓3)␈↓ αt ␈↓↓∀n.(n = 0 ∨ ␈↓	F␈↓↓(n␈↓∧-␈↓↓) ⊃ ␈↓	F␈↓↓(n)) ⊃ ∀n.␈↓	F␈↓↓(n)␈↓

␈↓ α∧␈↓These too correspond to the termination of certain recursively defined predicates, namely

␈↓ α∧␈↓4)␈↓ αt ␈↓↓issexp x ← ␈↓αa␈↓↓t x ∨ issexp ␈↓αa␈↓↓ x ∧ issexp ␈↓αd␈↓↓ x␈↓

␈↓ α∧␈↓for S-expressions, and

␈↓ α∧␈↓5)␈↓ αt ␈↓↓isnatnum n ← n=0 ∨ isnatnum n␈↓∧-␈↓.

␈↓ α∧␈↓for natural numbers.

␈↓ α∧␈↓␈↓ αTThe␈αneed␈αfor␈αthe␈αextra␈αvariable␈α␈↓↓u␈↓␈αin␈αgraph␈αinduction␈αcomes␈αfrom␈αthe␈αfact␈αthat␈αgraphs␈αare

␈↓ α∧␈↓not␈α⊃an␈α∩inductively␈α⊃defined␈α⊃set␈α∩in␈α⊃any␈α⊃obvious␈α∩sense.␈α⊃ The␈α⊃analogy␈α∩with␈α⊃relative␈α∩concepts␈α⊃in

␈↓ α∧␈↓topology, e.g. relative homology groups, may be suggestive.

␈↓ α∧␈↓␈↓ αTGraph␈α
induction␈α
can␈αbe␈α
informally␈α
justified␈α
by␈αregarding␈α
the␈α
rank␈α
of␈αan␈α
␈↓↓<x, u>␈↓␈α
pair␈αas␈α
the

␈↓ α∧␈↓number␈α
of␈α
nodes␈α
in␈α
the␈α
graph␈αnot␈α
included␈α
in␈α
␈↓↓u.␈↓␈α
If␈α
␈↓↓∀x.␈↓	F␈↓↓(x, u)␈↓␈αis␈α
false,␈α
then␈α
there␈α
is␈α
a␈αcounter
␈↓ α∧␈↓␈↓ u3


␈↓ α∧␈↓example␈α∞of␈α∂least␈α∞rank,␈α∞say␈α∂␈↓↓<x0, u0>␈↓.␈α∞ If␈α∞␈↓↓x0 ε u0␈↓␈α∂or␈α∞␈↓↓␈↓αa␈↓↓t x0,␈↓α␈α∞the␈α∂premisses␈α∞of␈α∞the␈α∂induction␈α∞are

␈↓ α∧␈↓αviolated.␈α Otherwise,␈α␈↓↓x0␈↓α␈αis␈αneither␈αatomic␈α
nor␈αin␈α␈↓↓u0.␈↓α␈αIf␈α␈↓↓␈↓	F␈↓↓(␈↓αa␈↓↓ x0, x0.u0) ∧ ␈↓	F␈↓↓(␈↓αd␈↓↓ x0, x0.u0)␈↓␈αis␈α
true,

␈↓ α∧␈↓the␈αthird␈αpremiss␈αof␈αthe␈αinduction␈αis␈αviolated.␈α But␈αthen␈αeither␈α␈↓↓␈↓	F␈↓↓(␈↓αa␈↓↓ x0, x0.u0)␈↓␈αor␈α␈↓↓␈↓	F␈↓↓(␈↓αd␈↓↓ x0, x0.u0)␈↓

␈↓ α∧␈↓would constitute a counter-example of lower rank.

␈↓ α∧␈↓␈↓ αTAs␈α
an␈αexample,␈α
we␈α
use␈αthe␈α
techniques␈α
of␈α(Cartwright␈α
1977)␈α
and␈αgraph␈α
induction␈α
to␈αprove

␈↓ α∧␈↓total the function

␈↓ α∧␈↓6)␈↓ αt ␈↓↓nodes[x,u] ← ␈↓αif␈↓↓ x ε u ␈↓αthen␈↓↓ u ␈↓αelse␈↓↓ ␈↓αif␈↓↓ ␈↓αa␈↓↓t x ␈↓αthen␈↓↓ x.u ␈↓αelse␈↓↓ nodes[␈↓αd␈↓↓ x, nodes[␈↓αa␈↓↓ x, u]]␈↓,

␈↓ α∧␈↓whose value is a list of nodes reachable from ␈↓↓x␈↓ that are not in the list ␈↓↓u.␈↓

␈↓ α∧␈↓␈↓ αTThe function ␈↓↓nodes␈↓ defined by the recursive program (6) satisfies the functional equation

␈↓ α∧␈↓7)␈↓ αt ␈↓↓∀x u.(nodes[x,u] = ␈↓αif␈↓↓ x ε u ␈↓αthen␈↓↓ u ␈↓αelse␈↓↓ ␈↓αif␈↓↓ ␈↓αa␈↓↓t x ␈↓αthen␈↓↓ x.u ␈↓αelse␈↓↓ nodes[␈↓αd␈↓↓ x, nodes[␈↓αa␈↓↓ x, u]])␈↓,

␈↓ α∧␈↓where␈α=␈αhas␈αreplaced␈α←,␈αand␈αthe␈αdomain␈αhas␈αbeen␈αextended␈αby␈αan␈αundefined␈αelement␈αtaken␈αto␈αbe

␈↓ α∧␈↓the value of a function when the computation doesn't terminate.  Hence

␈↓ α∧␈↓␈↓ αT␈↓↓∀x u.islist nodes[x,u]␈↓

␈↓ α∧␈↓is␈α∂the␈α∂assertion␈α∂that␈α∞for␈α∂all␈α∂nodes␈α∂␈↓↓x␈↓␈α∞and␈α∂lists␈α∂␈↓↓u␈↓␈α∂the␈α∞value␈α∂of␈α∂the␈α∂function␈α∞is␈α∂a␈α∂list,␈α∂i.e.␈α∂not␈α∞the

␈↓ α∧␈↓undefined␈α⊃element.␈α∩ This␈α⊃theory␈α∩is␈α⊃is␈α∩explained␈α⊃in␈α∩(Cartwright␈α⊃and␈α∩McCarthy␈α⊃1979)␈α∩and␈α⊃in

␈↓ α∧␈↓(McCarthy and Talcott 1980).

␈↓ α∧␈↓␈↓ αTTo make the induction work, we prove the more general statement

␈↓ α∧␈↓8)␈↓ αt ␈↓↓∀x u.(∀w. u ⊂ w ⊃ islist nodes[x,w] ∧ u ⊂ nodes[x,w])␈↓.

␈↓ α∧␈↓Here␈α␈↓↓u ⊂ v␈↓␈αmeans␈α
that␈αevery␈αelement␈αof␈α
the␈αlist␈α␈↓↓u␈↓␈αis␈α
a␈αmember␈αof␈αthe␈α
list␈α␈↓↓v,␈↓␈αand␈αour␈α
proof␈αuses

␈↓ α∧␈↓obvious␈α
properties␈αof␈α
⊂␈αwhich␈α
can␈αbe␈α
proved␈αby␈α
list␈αinduction␈α
from␈αa␈α
suitable␈αrecursive␈α
definition

␈↓ α∧␈↓of ␈↓↓u ⊂ v␈↓.

␈↓ α∧␈↓␈↓ αTWe now take

␈↓ α∧␈↓9)␈↓ αt ␈↓↓␈↓	F␈↓↓(x,u) ≡ ∀w.(u ⊂ w ⊃ islist nodes[x,w] ∧ u ⊂ nodes[x,w])␈↓.

␈↓ α∧␈↓and␈αprove␈α␈↓↓␈↓	F␈↓↓(x,u)␈↓␈α
assuming␈αsuccesively␈α␈↓↓x␈α
ε␈αu␈↓,␈α␈↓↓␈↓αa␈↓↓t␈α
x␈↓␈αand␈α␈↓↓␈↓	F␈↓↓(␈↓αa␈↓↓ x, u)␈↓ ∧ ␈↓↓␈↓	F␈↓↓(␈↓αa␈↓↓ x, u)␈↓␈α
as␈αis␈αrequired␈αto␈α
use

␈↓ α∧␈↓the schema (1).
␈↓ α∧␈↓␈↓ u4


␈↓ α∧␈↓␈↓ αTThe cases ␈↓↓x ε u␈↓ and ␈↓↓␈↓αa␈↓↓t x␈↓ are absolutely straightforward.  ␈↓↓␈↓	F␈↓↓(␈↓αa␈↓↓ x, x.u)␈↓ takes the form

␈↓ α∧␈↓␈↓ αT␈↓↓∀v.(x.u ⊂ v ⊃ islist nodes[␈↓αa␈↓↓ x, v] ∧ x.u ⊂ nodes[␈↓αa␈↓↓ x, v])␈↓,

␈↓ α∧␈↓and we specialize this by choosing ␈↓↓v = x.w␈↓, getting

␈↓ α∧␈↓␈↓ αT␈↓↓islist nodes[␈↓αa␈↓↓ x, x.w] ∧ x.u ⊂ nodes[␈↓αa␈↓↓ x, x.w]␈↓.

␈↓ α∧␈↓␈↓↓␈↓	F␈↓↓(␈↓αd␈↓↓ x, x.u)␈↓ takes the form

␈↓ α∧␈↓␈↓ αT␈↓↓∀v.(x.u ⊂ v ⊃ islist nodes[␈↓αd␈↓↓ x, v] ∧ x.u ⊂ nodes[␈↓αd␈↓↓ x, v]␈↓,

␈↓ α∧␈↓and we specialize it by choosing ␈↓↓v = nodes[␈↓αa␈↓↓ x, x.w]␈↓, getting eventually

␈↓ α∧␈↓␈↓ αT␈↓↓islist nodes[␈↓αd␈↓↓ x, nodes[␈↓αa␈↓↓ x, x.w]] ∧ u ⊂ nodes[␈↓αd␈↓↓ x, nodes[␈↓αa␈↓↓ x, x.w]]␈↓,

␈↓ α∧␈↓which is all we need to complete the proof.




␈↓ α∧␈↓αExercises:

␈↓ α∧␈↓␈↓ αTWrite and prove total programs as follows:

␈↓ α∧␈↓␈↓ αT1.␈α∞A␈α∞program␈α∞that␈α∞represents␈α∂a␈α∞graph␈α∞as␈α∞a␈α∞list␈α∞of␈α∂three␈α∞element␈α∞lists␈α∞of␈α∞atoms.␈α∂ For␈α∞each

␈↓ α∧␈↓non-atomic␈αnode␈αthere␈αis␈αa␈αlist␈αconsisting␈αof␈αthis␈αelement␈αfollowed␈αby␈αits␈α␈↓↓car␈↓␈αand␈αits␈α␈↓↓cdr.␈↓␈αOn␈αsuch

␈↓ α∧␈↓lists␈α
one␈α
can␈α
define␈α
operations␈α␈↓↓car1␈↓␈α
and␈α
␈↓↓cdr1␈↓␈α
and␈α
prove␈αthe␈α
isomorphism␈α
between␈α
them␈α
and␈α␈↓↓car␈↓

␈↓ α∧␈↓and␈α␈↓↓cd␈↓␈α
on␈αthe␈αoriginal␈α
graphs.␈α The␈αfact␈α
that␈α␈↓↓gensym()␈↓␈αis␈α
not␈αa␈αfunction␈α
in␈αthe␈αmathematical␈α
sense

␈↓ α∧␈↓has to be somehow finessed.

␈↓ α∧␈↓␈↓ αT2.␈αWrite␈αand␈α
prove␈αsome␈αfacts␈α
about␈αa␈αprogram␈αthat␈α
searches␈αa␈αgraph␈α
for␈αa␈αvertex␈α
with␈αa

␈↓ α∧␈↓given property.

␈↓ α∧␈↓␈↓ αT3. Write a program that tests graphs for isomorphisms of various kinds.




␈↓ α∧␈↓αReferences:

␈↓ α∧␈↓␈↓αCartwright,␈αR.S.␈α(1977)␈↓:␈α
␈↓↓A␈αPractical␈αFormal␈α
Semantic␈αDefinition␈αand␈α
Verification␈αSystem␈αfor␈α
Typed

␈↓ α∧␈↓↓Lisp␈↓, Ph.D. Thesis, Computer Science Department, Stanford University, Stanford, California.
␈↓ α∧␈↓␈↓ u5


␈↓ α∧␈↓␈↓αCartwright,␈α⊃Robert␈α⊂and␈α⊃John␈α⊂McCarthy␈α⊃(1979)␈↓:␈α⊃"Recursive␈α⊂Programs␈α⊃as␈α⊂Functions␈α⊃in␈α⊃a␈α⊂First

␈↓ α∧␈↓Order␈α∀Theory",␈α∃in␈α∀␈↓↓Proceedings␈α∃of␈α∀the␈α∃International␈α∀Conference␈α∃on␈α∀Mathematical␈α∃Studies␈α∀of

␈↓ α∧␈↓↓Information Processing␈↓, Kyoto, Japan.

␈↓ α∧␈↓␈↓αMcCarthy,␈α∞John␈α∂and␈α∞Carolyn␈α∂Talcott␈α∞(1980)␈↓:␈α∞␈↓↓LISP␈α∂-␈α∞Programming␈α∂and␈α∞Proving␈↓,␈α∂course␈α∞notes,

␈↓ α∧␈↓Stanford University. (to be published as a book).

␈↓ α∧␈↓␈↓αMorris,␈αL.␈αand␈αJ.␈αSchwarz␈α(1980)␈↓:␈α"Computing␈αCyclic␈αList␈αStructures",␈αin␈α␈↓↓Conference␈αRecord␈αof␈αthe

␈↓ α∧␈↓↓1980 LISP Conference␈↓, The LISP Conference, P.O. Box 487, Redwood Estates, CA 95044.

␈↓ α∧␈↓This version of CYCLIC[E80,JMC] pubbed on September 12, 1980.